#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "ksat.h"

struct ksat* init_ksat (void)
{
	struct ksat* ksat = (struct ksat *) malloc (sizeof (struct ksat));

	ksat->num_clauses = 0;
	ksat->max_clauses = 1000;
	ksat->num_variables = 1;
	ksat->clause = calloc (ksat->max_clauses, sizeof (struct clause));
	if (ksat->clause == NULL)
	{
		printf ("calloc failed\n");
		exit (-1);
	}

	return ksat;
}

void free_ksat (struct ksat *ksat)
{
	int i;

	for (i = 0; i < ksat->num_clauses; i++)
	{
		free (ksat->clause[i].list);
	}

	free (ksat->clause);
	free (ksat);
}

void add_clause (struct ksat *ksat, int k, int list[k])
{
	if (ksat->num_clauses == ksat->max_clauses)
	{
		ksat->max_clauses += 1000;
		ksat->clause = realloc (ksat->clause, ksat->max_clauses * sizeof (struct clause));
		if (ksat->clause == NULL)
		{
			printf ("realloc failed\n");
			exit (-1);
		}
	}

	ksat->clause[ksat->num_clauses].k = k;
	ksat->clause[ksat->num_clauses].list = calloc (k, sizeof (int));
	if (ksat->clause[ksat->num_clauses].list == NULL)
	{
		printf ("calloc failed\n");
		exit (-1);
	}

	memcpy (ksat->clause[ksat->num_clauses].list, list, k * sizeof (int));

	ksat->num_clauses ++;
}

void print_ksat (struct ksat *ksat)
{
	int i, j;

	printf ("p cnf %d %d\n", ksat->num_variables, ksat->num_clauses);
	
	for (i = 0; i < ksat->num_clauses; i++)
	{
		for (j = 0; j < ksat->clause[i].k; j++)
		{
			printf ("%d ", ksat->clause[i].list[j]);
		}
		printf ("0\n");
	}
}
